inv{-}rel($A$;$B$;$f$;${\it finv}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\forall$$a$:$A$, $b$:$B$. ${\it finv}$($b$) $=$ inl($a$) $\Rightarrow$ $b$ $=$ $f$($a$)) \& ($\forall$$a$:$A$. ${\it finv}$($f$($a$)) $=$ inl($a$))